(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Sun Microsystems Inc.) Main-Class: TypeSwitch
public class A {
public boolean hasSuperType() {
return false;
}

public A getSuperType() {
return null;
}
}


public class B extends A {
public boolean hasSuperType() {
return true;
}

public A getSuperType() {
return new A();
}
}


public class C extends B {
public A getSuperType() {
return new B();
}
}


public class TypeSwitch {
public static void main(String[] args) {
A x = null;
switch (args.length) {
case 0: x = new A();
break;
case 1: x = new B();
break;
case 2: x = new C();
break;
}

while (x.hasSuperType()) {
x = x.getSuperType();
}
}
}


(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
TypeSwitch.main([Ljava/lang/String;)V: Graph of 142 nodes with 0 SCCs.


(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

(4) TRUE